/*
 * Copyright 2014, General Dynamics C4 Systems
 *
 * SPDX-License-Identifier: GPL-2.0-only
 */

#include <config.h>
#include <types.h>
#include <api/failures.h>
#include <kernel/vspace.h>
#include <object/structures.h>
#include <arch/machine.h>
#include <arch/model/statedata.h>
#include <machine/fpu.h>
#include <arch/object/objecttype.h>
#include <arch/object/ioport.h>
#include <plat/machine/devices.h>

#include <arch/object/iospace.h>
#include <arch/object/vcpu.h>
#include <plat/machine/intel-vtd.h>
/*Z 拷贝架构相关的能力。基本是原能力，要作一些排错、复位等处理 */
deriveCap_ret_t Arch_deriveCap(cte_t *slot, cap_t cap)
{
    deriveCap_ret_t ret;

    switch (cap_get_capType(cap)) {
    case cap_page_table_cap:
        if (cap_page_table_cap_get_capPTIsMapped(cap)) {
            ret.cap = cap;
            ret.status = EXCEPTION_NONE;
        } else {
            userError("Deriving an unmapped PT cap");
            current_syscall_error.type = seL4_IllegalOperation;
            ret.cap = cap_null_cap_new();
            ret.status = EXCEPTION_SYSCALL_ERROR;/*Z 拷贝未映射的页能力导致系统调用错误 */
        }
        return ret;

    case cap_page_directory_cap:
        if (cap_page_directory_cap_get_capPDIsMapped(cap)) {
            ret.cap = cap;
            ret.status = EXCEPTION_NONE;
        } else {    /*Z 不好：错误信息不一致，虽然未映射与未赋予ASID基本一个意思 */
            userError("Deriving a PD cap without an assigned ASID");
            current_syscall_error.type = seL4_IllegalOperation;
            ret.cap = cap_null_cap_new();
            ret.status = EXCEPTION_SYSCALL_ERROR;
        }
        return ret;

    case cap_asid_control_cap:
    case cap_asid_pool_cap:
        ret.cap = cap;
        ret.status = EXCEPTION_NONE;
        return ret;
    case cap_io_port_control_cap:
        ret.status = EXCEPTION_NONE;
        ret.cap = cap_null_cap_new();/*Z IO端口分配能力只能有一个 */
        return ret;
    case cap_io_port_cap:
        ret.cap = cap;
        ret.status = EXCEPTION_NONE;
        return ret;

#ifdef CONFIG_IOMMU
    case cap_io_space_cap:
        ret.cap = cap;
        ret.status = EXCEPTION_NONE;
        return ret;
    case cap_io_page_table_cap:
        if (cap_io_page_table_cap_get_capIOPTIsMapped(cap)) {
            ret.cap = cap;
            ret.status = EXCEPTION_NONE;
        } else {/*Z 不好：这里为什么没有userError */
            current_syscall_error.type = seL4_IllegalOperation;
            ret.cap = cap_null_cap_new();
            ret.status = EXCEPTION_SYSCALL_ERROR;
        }
        return ret;
#endif

#ifdef CONFIG_VTX
    case cap_vcpu_cap:
        ret.cap = cap;
        ret.status = EXCEPTION_NONE;
        return ret;
    case cap_ept_pml4_cap:
        if (cap_ept_pml4_cap_get_capPML4IsMapped(cap)) {
            ret.cap = cap;
            ret.status = EXCEPTION_NONE;
        } else {    /*Z 不好：错误信息不一致，虽然未映射与未赋予ASID基本一个意思 */
            userError("Deriving a EPT PML4 cap without an assigned ASID.");
            current_syscall_error.type = seL4_IllegalOperation;
            ret.cap = cap_null_cap_new();
            ret.status = EXCEPTION_SYSCALL_ERROR;
        }
        return ret;
    case cap_ept_pdpt_cap:
        if (cap_ept_pdpt_cap_get_capPDPTIsMapped(cap)) {
            ret.cap = cap;
            ret.status = EXCEPTION_NONE;
        } else {
            userError("Deriving an unmapped EPT PDPT cap.");
            current_syscall_error.type = seL4_IllegalOperation;
            ret.cap = cap_null_cap_new();
            ret.status = EXCEPTION_SYSCALL_ERROR;
        }
        return ret;

    case cap_ept_pd_cap:
        if (cap_ept_pd_cap_get_capPDIsMapped(cap)) {
            ret.cap = cap;
            ret.status = EXCEPTION_NONE;
        } else {
            userError("Deriving an unmapped EPT PD cap.");
            current_syscall_error.type = seL4_IllegalOperation;
            ret.cap = cap_null_cap_new();
            ret.status = EXCEPTION_SYSCALL_ERROR;
        }
        return ret;

    case cap_ept_pt_cap:
        if (cap_ept_pt_cap_get_capPTIsMapped(cap)) {
            ret.cap = cap;
            ret.status = EXCEPTION_NONE;
        } else {
            userError("Deriving an unmapped EPT PT cap.");
            current_syscall_error.type = seL4_IllegalOperation;
            ret.cap = cap_null_cap_new();
            ret.status = EXCEPTION_SYSCALL_ERROR;
        }
        return ret;
#endif

    default:
        return Mode_deriveCap(slot, cap);
    }
}
/*Z 更新能力的参数，可能得到空能力。preserve指示是否保持原参数 */
cap_t CONST Arch_updateCapData(bool_t preserve, word_t data, cap_t cap)
{
    /* Avoid a switch statement with just a 'default' case as the C parser does not like this */
#ifdef CONFIG_IOMMU
    switch (cap_get_capType(cap)) {
    case cap_io_space_cap: {
        io_space_capdata_t w = { { data } };
        uint16_t PCIDevice = io_space_capdata_get_PCIDevice(w);
        uint16_t domainID = io_space_capdata_get_domainID(w);
        if (!preserve && cap_io_space_cap_get_capPCIDevice(cap) == 0 &&/*Z 原参数不保留，且未关联PCI设备，才可能更新 */
            domainID >= x86KSFirstValidIODomain &&
            domainID != 0                        &&
            domainID <= MASK(x86KSnumIODomainIDBits)) {/*Z 更新域、PCI设备编码 */
            return cap_io_space_cap_new(domainID, PCIDevice);
        } else {
            return cap_null_cap_new();
        }
    }

    default:
        return cap;
    }
#endif
    return cap;
}
/*Z 根据掩码设置能力最后的权限 */
cap_t CONST Arch_maskCapRights(seL4_CapRights_t cap_rights_mask, cap_t cap)
{
    if (cap_get_capType(cap) == cap_frame_cap) {
        vm_rights_t vm_rights;

        vm_rights = vmRightsFromWord(cap_frame_cap_get_capFVMRights(cap));
        vm_rights = maskVMRights(vm_rights, cap_rights_mask);/*Z 根据掩码确定最后的读写权限 */
        return cap_frame_cap_set_capFVMRights(cap, wordFromVMRights(vm_rights));
    } else {
        return cap;
    }
}
/*Z 根据能力种类做不同的清理工作。注意：如页表等只是清除页表项，并没回收内存。剩余为空，后续清理可能不为空 */
finaliseCap_ret_t Arch_finaliseCap(cap_t cap, bool_t final)
{
    finaliseCap_ret_t fc_ret;

    switch (cap_get_capType(cap)) {
    case cap_page_directory_cap:
        if (final && cap_page_directory_cap_get_capPDIsMapped(cap)) {
            unmapPageDirectory(/*Z 删除三级页表在二级页表中的表项 */
                cap_page_directory_cap_get_capPDMappedASID(cap),
                cap_page_directory_cap_get_capPDMappedAddress(cap),
                PDE_PTR(cap_page_directory_cap_get_capPDBasePtr(cap))
            );
        }
        break;

    case cap_page_table_cap:
        if (final && cap_page_table_cap_get_capPTIsMapped(cap)) {
            unmapPageTable(/*Z 删除四级页表在三级页表中的表项 */
                cap_page_table_cap_get_capPTMappedASID(cap),
                cap_page_table_cap_get_capPTMappedAddress(cap),
                PT_PTR(cap_page_table_cap_get_capPTBasePtr(cap))
            );
        }
        break;

    case cap_asid_pool_cap:
        if (final) {
            deleteASIDPool(/*Z 置空指定的ASID(PCID) pool */
                cap_asid_pool_cap_get_capASIDBase(cap),
                ASID_POOL_PTR(cap_asid_pool_cap_get_capASIDPool(cap))
            );
        }
        break;
    case cap_asid_control_cap:
    case cap_io_port_control_cap:
        break;
    case cap_io_port_cap:
#ifdef CONFIG_VTX   /*Z 禁用vcpu指定范围的I/O端口 */
        clearVPIDIOPortMappings(cap_io_port_cap_get_capIOPortVPID(cap),
                                cap_io_port_cap_get_capIOPortFirstPort(cap),
                                cap_io_port_cap_get_capIOPortLastPort(cap));
#endif
        if (final) {
            fc_ret.remainder = cap_null_cap_new();
            fc_ret.cleanupInfo = cap;/*Z 还有后续清理工作 */
            return fc_ret;
        }
        break;
#ifdef CONFIG_IOMMU
    case cap_io_space_cap:
        if (final) {/*Z 删除IOMMU上下文表中能力对应的表项 */
            unmapVTDContextEntry(cap);
        }
        break;

    case cap_io_page_table_cap:/*Z 能力中设置成未映射(无效)，并将该页表层级中一级页表虚拟地址映射项置空 */
        if (final && cap_io_page_table_cap_get_capIOPTIsMapped(cap)) {
            deleteIOPageTable(cap);
        }
        break;
#endif

#ifdef CONFIG_VTX
    case cap_vcpu_cap:
        if (final) {/*Z 取消VCPU关联的线程，清除正运行的环境(虚拟cpu不再活跃、相关数据未加载、VMCS清除) */
            vcpu_finalise(VCPU_PTR(cap_vcpu_cap_get_capVCPUPtr(cap)));
        }
        break;
    case cap_ept_pml4_cap:/*Z 清除EPT一级页表在ASID(PCID) pool中的映射项 */
        if (final && cap_ept_pml4_cap_get_capPML4IsMapped(cap)) {
            deleteEPTASID(cap_ept_pml4_cap_get_capPML4MappedASID(cap),
                          (ept_pml4e_t *)cap_ept_pml4_cap_get_capPML4BasePtr(cap));
        }
        break;

    case cap_ept_pdpt_cap:
        if (final && cap_ept_pdpt_cap_get_capPDPTIsMapped(cap)) {
            unmapEPTPDPT(/*Z 清除EPT二级页表的一级页表项 */
                cap_ept_pdpt_cap_get_capPDPTMappedASID(cap),
                cap_ept_pdpt_cap_get_capPDPTMappedAddress(cap),
                (ept_pdpte_t *)cap_ept_pdpt_cap_get_capPDPTBasePtr(cap));
        }
        break;

    case cap_ept_pd_cap:
        if (final && cap_ept_pd_cap_get_capPDIsMapped(cap)) {
            unmapEPTPageDirectory(/*Z 清除EPT三级页表的二级页表项 */
                cap_ept_pd_cap_get_capPDMappedASID(cap),
                cap_ept_pd_cap_get_capPDMappedAddress(cap),
                (ept_pde_t *)cap_ept_pd_cap_get_capPDBasePtr(cap));
        }
        break;

    case cap_ept_pt_cap:
        if (final && cap_ept_pt_cap_get_capPTIsMapped(cap)) {
            unmapEPTPageTable(/*Z 清除EPT四级页表的三级页表项 */
                cap_ept_pt_cap_get_capPTMappedASID(cap),
                cap_ept_pt_cap_get_capPTMappedAddress(cap),
                (ept_pte_t *)cap_ept_pt_cap_get_capPTBasePtr(cap));
        }
        break;
#endif

    default:/*Z 对页能力清除页表映射，对页表能力当final为真时清除上级页表项(ASID pool项) */
        return Mode_finaliseCap(cap, final);
    }

    fc_ret.remainder = cap_null_cap_new();
    fc_ret.cleanupInfo = cap_null_cap_new();
    return fc_ret;
}
/*Z 能力a所指内存是否与b所指的相同。有特殊情况，见内容 */
bool_t CONST Arch_sameRegionAs(cap_t cap_a, cap_t cap_b)
{
    switch (cap_get_capType(cap_a)) {
    case cap_frame_cap:
        if (cap_get_capType(cap_b) == cap_frame_cap) {/*Z a的包含b的视为相同 */
            word_t botA, botB, topA, topB;
            botA = cap_frame_cap_get_capFBasePtr(cap_a);
            botB = cap_frame_cap_get_capFBasePtr(cap_b);
            topA = botA + MASK(pageBitsForSize(cap_frame_cap_get_capFSize(cap_a)));
            topB = botB + MASK(pageBitsForSize(cap_frame_cap_get_capFSize(cap_b)));
            return ((botA <= botB) && (topA >= topB) && (botB <= topB));
        }
        break;

    case cap_page_table_cap:
        if (cap_get_capType(cap_b) == cap_page_table_cap) {
            return cap_page_table_cap_get_capPTBasePtr(cap_a) ==
                   cap_page_table_cap_get_capPTBasePtr(cap_b);
        }
        break;

    case cap_page_directory_cap:
        if (cap_get_capType(cap_b) == cap_page_directory_cap) {
            return cap_page_directory_cap_get_capPDBasePtr(cap_a) ==
                   cap_page_directory_cap_get_capPDBasePtr(cap_b);
        }
        break;

    case cap_asid_control_cap:/*Z 能力相同即视为相同 */
        if (cap_get_capType(cap_b) == cap_asid_control_cap) {
            return true;
        }
        break;

    case cap_asid_pool_cap:
        if (cap_get_capType(cap_b) == cap_asid_pool_cap) {
            return cap_asid_pool_cap_get_capASIDPool(cap_a) ==
                   cap_asid_pool_cap_get_capASIDPool(cap_b);
        }
        break;

    case cap_io_port_control_cap:/*Z IO端口控制能力与该能力、或与IO端口能力视为相同，反之不然，见下条 */
        if (cap_get_capType(cap_b) == cap_io_port_control_cap ||
            cap_get_capType(cap_b) == cap_io_port_cap) {
            return true;
        }
        break;

    case cap_io_port_cap:/*Z IO端口能力所指端口范围完全相同则视为相同 */
        if (cap_get_capType(cap_b) == cap_io_port_cap) {
            return  cap_io_port_cap_get_capIOPortFirstPort(cap_a) ==
                    cap_io_port_cap_get_capIOPortFirstPort(cap_b) &&
                    cap_io_port_cap_get_capIOPortLastPort(cap_a) ==
                    cap_io_port_cap_get_capIOPortLastPort(cap_b);
        }
        break;

#ifdef CONFIG_IOMMU
    case cap_io_space_cap:/*Z IO空间能力设备相同视为相同 */
        if (cap_get_capType(cap_b) == cap_io_space_cap) {
            return cap_io_space_cap_get_capPCIDevice(cap_a) ==
                   cap_io_space_cap_get_capPCIDevice(cap_b);
        }
        break;

    case cap_io_page_table_cap:
        if (cap_get_capType(cap_b) == cap_io_page_table_cap) {
            return cap_io_page_table_cap_get_capIOPTBasePtr(cap_a) ==
                   cap_io_page_table_cap_get_capIOPTBasePtr(cap_b);
        }
        break;
#endif

#ifdef CONFIG_VTX
    case cap_vcpu_cap:
        if (cap_get_capType(cap_b) == cap_vcpu_cap) {
            return cap_vcpu_cap_get_capVCPUPtr(cap_a) ==
                   cap_vcpu_cap_get_capVCPUPtr(cap_b);
        }
        break;

    case cap_ept_pml4_cap:
        if (cap_get_capType(cap_b) == cap_ept_pml4_cap) {
            return cap_ept_pml4_cap_get_capPML4BasePtr(cap_a) ==
                   cap_ept_pml4_cap_get_capPML4BasePtr(cap_b);
        }
        break;

    case cap_ept_pdpt_cap:
        if (cap_get_capType(cap_b) == cap_ept_pdpt_cap) {
            return cap_ept_pdpt_cap_get_capPDPTBasePtr(cap_a) ==
                   cap_ept_pdpt_cap_get_capPDPTBasePtr(cap_b);
        }
        break;

    case cap_ept_pd_cap:
        if (cap_get_capType(cap_b) == cap_ept_pd_cap) {
            return cap_ept_pd_cap_get_capPDBasePtr(cap_a) ==
                   cap_ept_pd_cap_get_capPDBasePtr(cap_b);
        }
        break;

    case cap_ept_pt_cap:
        if (cap_get_capType(cap_b) == cap_ept_pt_cap) {
            return cap_ept_pt_cap_get_capPTBasePtr(cap_a) ==
                   cap_ept_pt_cap_get_capPTBasePtr(cap_b);
        }
        break;

#endif

    }

    return Mode_sameRegionAs(cap_a, cap_b);
}
/*Z 两个能力指的是否同一对象 */
bool_t CONST Arch_sameObjectAs(cap_t cap_a, cap_t cap_b)
{
    if (cap_get_capType(cap_a) == cap_io_port_control_cap &&
        cap_get_capType(cap_b) == cap_io_port_cap) {
        return false;
    }
    if (cap_get_capType(cap_a) == cap_frame_cap) {/*Z 地址、大小、设备内存标识都要相同 */
        if (cap_get_capType(cap_b) == cap_frame_cap) {
            return ((cap_frame_cap_get_capFBasePtr(cap_a) ==
                     cap_frame_cap_get_capFBasePtr(cap_b)) &&
                    (cap_frame_cap_get_capFSize(cap_a) ==
                     cap_frame_cap_get_capFSize(cap_b)) &&
                    ((cap_frame_cap_get_capFIsDevice(cap_a) == 0) ==
                     (cap_frame_cap_get_capFIsDevice(cap_b) == 0)));
        }
    }
    return Arch_sameRegionAs(cap_a, cap_b);
}
/*Z 返回seL4内核指定类型对象的大小(位数表示) */
word_t Arch_getObjectSize(word_t t)
{
    switch (t) {
    case seL4_X86_4K:
        return pageBitsForSize(X86_SmallPage);
    case seL4_X86_LargePageObject:
        return pageBitsForSize(X86_LargePage);
    case seL4_X86_PageTableObject:
        return seL4_PageTableBits;
    case seL4_X86_PageDirectoryObject:
        return seL4_PageDirBits;
    case seL4_IA32_PDPTObject:
        return seL4_PDPTBits;
    case seL4_X86_IOPageTableObject:
        return seL4_IOPageTableBits;
#ifdef CONFIG_VTX
    case seL4_X86_VCPUObject:
        return seL4_X86_VCPUBits;
    case seL4_X86_EPTPML4Object:
        return seL4_X86_EPTPML4Bits;
    case seL4_X86_EPTPDPTObject:
        return seL4_X86_EPTPDPTBits;
    case seL4_X86_EPTPDObject:
        return seL4_X86_EPTPDBits;
    case seL4_X86_EPTPTObject:
        return seL4_X86_EPTPTBits;
#endif
    default:
        return Mode_getObjectSize(t);
    }
}
/*Z 用指定的空闲内存创建指定的seL4内核对象，返回新对象的操控能力 */
cap_t Arch_createObject(object_t t, void *regionBase, word_t userSize, bool_t deviceMemory)
{                           /*Z 对象类型、空闲块地址、要求的对象大小、是否设备内存 */
#ifdef CONFIG_VTX
    switch (t) {
    case seL4_X86_VCPUObject: {
        vcpu_t *vcpu;
        vcpu = VCPU_PTR((word_t)regionBase);
        vcpu_init(vcpu);/*Z 初始化VCPU数据结构，返回cap_vcpu_cap能力 */
        return cap_vcpu_cap_new(VCPU_REF(vcpu));
    }
    case seL4_X86_EPTPML4Object:/*Z 返回未映射(无效)、无VPID的cap_ept_pml4_cap能力 */
        return cap_ept_pml4_cap_new(
                   0,                  /* capPML4IsMapped      *//*Z 未映射(无效) */
                   VPID_INVALID,       /* capPML4MappedASID    *//*Z 无VPID */
                   (word_t)regionBase  /* capPML4BasePtr       */
               );
    case seL4_X86_EPTPDPTObject:/*Z 返回未映射(无效)、无VPID的cap_ept_pdpt_cap能力 */
        return cap_ept_pdpt_cap_new(
                   0,                  /* capPDPTMappedAddress */
                   0,                  /* capPDPTIsMapped      */
                   VPID_INVALID,       /* capPDPTMappedASID    */
                   (word_t)regionBase   /* capPDPTBasePtr      */
               );
    case seL4_X86_EPTPDObject:/*Z 返回未映射(无效)、无VPID的cap_ept_pd_cap能力 */
        return cap_ept_pd_cap_new(
                   0,                  /* capPDMappedAddress   */
                   0,                  /* capPDIsMapped        */
                   VPID_INVALID,       /* capPDMappedASID      */
                   (word_t)regionBase  /* capPDBasePtr         */
               );
    case seL4_X86_EPTPTObject:/*Z 返回未映射(无效)、无VPID的cap_ept_pt_cap能力 */
        return cap_ept_pt_cap_new(
                   0,                  /* capPTMappedAddress   */
                   0,                  /* capPTIsMapped        */
                   VPID_INVALID,       /* capPTMappedASID      */
                   (word_t)regionBase  /* capPTBasePtr         */
               );
    default:
#endif
        return Mode_createObject(t, regionBase, userSize, deviceMemory);
#ifdef CONFIG_VTX
    }
#endif
}
/*Z 主动类系统调用处理函数 */
exception_t Arch_decodeInvocation(/*Z 系统调用传入的当前线程参数：*/
    word_t invLabel,        /*Z 消息标签(错误类型) */
    word_t length,          /*Z 消息长度 */
    cptr_t cptr,            /*Z CSlot句柄 */
    cte_t *slot,            /*Z 其CSlot */
    cap_t cap,              /*Z 其能力 */
    extra_caps_t excaps,    /*Z 额外能力 */
    bool_t call,            /*Z 是否Call调用 */
    word_t *buffer          /*Z IPC buffer */
)
{
    switch (cap_get_capType(cap)) {
    case cap_asid_control_cap:
    case cap_asid_pool_cap:
        return decodeX86MMUInvocation(invLabel, length, cptr, slot, cap, excaps, buffer);
    case cap_io_port_control_cap:/*Z 为CNode分配空闲端口 */
        return decodeX86PortControlInvocation(invLabel, length, cptr, slot, cap, excaps, buffer);
    case cap_io_port_cap:/*Z I/O端口输入、输出*/
        return decodeX86PortInvocation(invLabel, length, cptr, slot, cap, excaps, call, buffer);
#ifdef CONFIG_IOMMU
    case cap_io_space_cap:/*Z 不支持 */
        return decodeX86IOSpaceInvocation(invLabel, cap);
    case cap_io_page_table_cap:/*Z 映射、解映射IO页表 */
        return decodeX86IOPTInvocation(invLabel, length, slot, cap, excaps, buffer);
#endif
#ifdef CONFIG_VTX
    case cap_vcpu_cap:
        return decodeX86VCPUInvocation(invLabel, length, cptr, slot, cap, excaps, buffer);
    case cap_ept_pml4_cap:
    case cap_ept_pdpt_cap:
    case cap_ept_pd_cap:
    case cap_ept_pt_cap:/*Z 映射、解映射EPT二、三、四级页表 */
        return decodeX86EPTInvocation(invLabel, length, cptr, slot, cap, excaps, buffer);
#endif
    default:/*Z 主要是MMU有关的映射、解映射 */
        return Mode_decodeInvocation(invLabel, length, cptr, slot, cap, excaps, buffer);
    }
}
/*Z 删除线程的活跃FPU环境 */
void Arch_prepareThreadDelete(tcb_t *thread)
{
    /* Notify the lazy FPU module about this thread's deletion. */
    fpuThreadDelete(thread);
}
/*Z 对I/O端口访问能力，清除已分配I/O端口位图全局变量中的位 */
void Arch_postCapDeletion(cap_t cap)
{
    if (cap_get_capType(cap) == cap_io_port_cap) {
        uint16_t first_port = cap_io_port_cap_get_capIOPortFirstPort(cap);
        uint16_t last_port = cap_io_port_cap_get_capIOPortLastPort(cap);
        /*Z 清除已分配I/O端口位图全局变量中，指定范围的I/O端口位 */
        freeIOPortRange(first_port, last_port);
    }
}
